the_w:World, e, e':E. FairFifo  e <c e'  Prop 

latex

Definitions	World, t  T, x:A. B(x), E, FairFifo, Type, P  Q, sender(e), s = t, kind(e), isrcv(k), b, A & B, e <loc e', left+right, P  Q, x:AB(x), x.A(x), R^+, f(a), x f y, e <c e'
Lemmas	rel plus wf, w-locl wf, assert wf, isrcv wf, w-ekind wf, w-sender wf, fair-fifo wf, w-E wf, world wf